3 if [ "x$BASH_SOURCE" == "x" ]; then echo '$BASH_SOURCE not set'; exit 1; fi
4 DEV
=$
(cd -P "$(dirname "${BASH_SOURCE[0]}" )" && pwd)
6 set -e # DO NOT USE PIPES unless this is rewritten
8 .
"$DEV/includes/php.sh"
10 if [ "x$PHP" != "x" -a -x "$PHP" ]; then
11 echo "PHP is already installed"
17 PHPURL
="https://secure.php.net/get/$TAR/from/this/mirror"
21 echo "Preparing to download and install a local copy of PHP $VER, note that this can take some time to do."
22 echo "If you wish to avoid re-doing this for future dev installations of MediaWiki we suggest installing php in ~/.mediawiki/php"
23 echo -n "Install PHP in ~/.mediawiki/php [y/N]: "
26 case "$INSTALLINHOME" in
28 PREFIX
="$HOME/.mediawiki/php"
35 # Some debian-like systems bundle wget but not curl, some other systems
36 # like os x bundle curl but not wget... use whatever is available
37 echo -n "Downloading PHP $VER"
38 if command -v wget
&>/dev
/null
; then
40 wget
-O "$TAR" "$PHPURL"
41 elif command -v curl
&>/dev
/null
; then
43 curl
"$PHPURL" -L -o "$TAR"
46 echo "Could not find curl or wget." >&2;
50 echo "Extracting php $VER"
55 echo "Configuring and installing php $VER in $PREFIX"
56 .
/configure
--prefix="$PREFIX"